COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.ss Induction on rank and the transfinite ordinal numbers
C00004 00003		In many proofs, the key step is formulating a mathematical
C00006 00004		The main step of most proofs of program correctness is the
C00009 ENDMK
C⊗;
.ss Induction on rank and the transfinite ordinal numbers


	As we have seen, almost any non-trivial proof about programs
involves a mathematical induction.  While ordinary induction on
natural numbers is often sufficient, it is usually more convenient
to use a more general form of induction.  Suppose the statement to
be proved involves variables x1, ... , xn, i.e. we want to prove
%2∀x1 ... xn.P(x1, ... ,xn)%1.  We introduce a function called
%2rank(x1, ... , xn)%1, and we prove %2P(x1, ... , xn)%1 under the
hypothesis that it is true for all n-tuplets of lower rank.  We
then wish to conclude that the statement is true for all n-tuplets.
The simplest case  occurs when the values of %2rank(x1,_..._,xn)%1
is a non-negative integer.
	In many proofs, the key step is formulating a mathematical
induction, and often the induction must be of a more general kind than the
integer inductions we study in college mathematics.  We must prove a
general statement that has many cases.  We introduce a function of the case
called its %2rank%1.  We show that our statement is true in an arbitrary
case provided it is true for all cases of lower rank.  We then want to
conclude that the statement is true in all cases.

	For this reasoning to be correct, ranks must be ordered, and the
rank must satisfy what mathematicians call a %2descending chain
condition%1, i.e. there must be no infinite descending chains of ranks
%2c1 > c2 > ... > cn > ..., etc.%1.  We are using the ordinary symbols
for our ordering, but we won't presume that our ranks are numbers.
They might, for example, be lists where ⊗u1 is considered less than
⊗u2 if it is a tail of ⊗u2. 

	Formally, we write this as follows:
	The main step of most proofs of program correctness is the
induction step.  A suitable sentence is proved under the hypothesis that
it is true for all ⊗simpler cases.  We then want to conclude that it is
always true.  This reasoning is valid provided that the notion of ⊗simpler
doesn't admit infinite chains of simpler and simpler cases.

	Indeed suppose that we have proved that the sentence is
true provided it is true for all simpler cases, and suppose that
it is nevertheless not always true, i.e. there is a counterexample.
If there were no simpler cases than the counterexample at all, then
it couldn't be a counterexample, because in proving the sentence
under the hypothesis that it is true for all simpler cases, we
have %2a fortiori%1 proved it when there are no simpler cases.
Therefore, if there is a counterexample, there must be a simpler
counterexample, and so a still simpler counterexample, and
even an infinite chain of ever simpler counterexamples.  However,
if the simplicity order admits no infinite descending chains at all,
then there couldn't be an infinite descending chain of counterexamples.

	Our present objective is to formalize this notion of
inductive proof in a general way.
The notion of %2transfinite ordinal number%1 will be
important.

	We begin by discussing the notion of ordering for which
we will use the ordinary symbols _<_ and _≤.  We will also use
_>_ and _≥_ when we want to write the ordering
relations in the reverse order.  An ordering
satisfies the following axioms:

	∀x y.(x ≤ y ≡ x < y ∨ x = y)

	∀x y.(x < y ⊃ x ≠ y)

	∀x y z.(x < y ∧ y < z ⊃ x < z).

These imply the transitivity of _≤, i.e.

	∀x y z.(x ≤ y ∧ y ≤ z ⊃ x ≤ z).

We do not now assume that the ordering is total, i.e. there might
exist elements ⊗x and ⊗y such that none of _%2x_<_y%1, _%2x_=_y%1
and _%2y_<_x%1 hold.